\begin{tabbing}
$\forall$\=$X$:Type$_{\mbox{\scriptsize j}}$, ${\it ds}$:$x$:Id fp$\rightarrow$ Type$_{\mbox{\scriptsize i}}$, ${\it da}$:$k$:Knd fp$\rightarrow$ Type$_{\mbox{\scriptsize i}}$, $x$:ecl(${\it ds}$;${\it da}$),\+
\\[0ex]${\it base}$:($k$:Knd$\rightarrow$(State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;$k$)$\rightarrow\mathbb{B}$)$\rightarrow$$X$), ${\it seq}$, ${\it and}$,
\\[0ex]${\it or}$:(ecl(${\it ds}$;${\it da}$)$\rightarrow$ecl(${\it ds}$;${\it da}$)$\rightarrow$$X$$\rightarrow$$X$$\rightarrow$$X$), ${\it repeat}$:(ecl(${\it ds}$;${\it da}$)$\rightarrow$$X$$\rightarrow$$X$), ${\it act}$,
\\[0ex]${\it throw}$:(ecl(${\it ds}$;${\it da}$)$\rightarrow\mathbb{N}\rightarrow$$X$$\rightarrow$$X$), ${\it catch}$:(ecl(${\it ds}$;${\it da}$)$\rightarrow$($\mathbb{N}$ List)$\rightarrow$$X$$\rightarrow$$X$).
\-\\[0ex]ecl\_ind($x$;$k$,${\it test}$.${\it base}$\=($k$\+
\\[0ex],${\it test}$);$a$,$b$,${\it rec}_{1}$,${\it rec}_{2}$.${\it seq}$\=($a$\+
\\[0ex],$b$
\\[0ex],${\it rec}_{1}$
\\[0ex],${\it rec}_{2}$);$a$,$b$,${\it rec}_{1}$,${\it rec}_{2}$.${\it and}$\=($a$\+
\\[0ex],$b$
\\[0ex],${\it rec}_{1}$
\\[0ex],${\it rec}_{2}$);$a$,$b$,${\it rec}_{1}$,${\it rec}_{2}$.${\it or}$\=($a$\+
\\[0ex],$b$
\\[0ex],${\it rec}_{1}$
\\[0ex],${\it rec}_{2}$);$a$,${\it rec}_{1}$.${\it repeat}$\=($a$\+
\\[0ex],${\it rec}_{1}$);$a$,$n$,${\it rec}_{1}$.${\it act}$\=($a$\+
\\[0ex],$n$
\\[0ex],${\it rec}_{1}$);$a$,$n$,${\it rec}_{1}$.${\it throw}$\=($a$\+
\\[0ex],$n$
\\[0ex],${\it rec}_{1}$);$a$,$l$,${\it rec}_{1}$.${\it catch}$\=($a$\+
\\[0ex],$l$
\\[0ex],${\it rec}_{1}$))
\-\-\-\-\-\-\-\-\\[0ex]$\in$ $X$
\end{tabbing}